
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "arithmetics/nat.ma".

inductive Formula: Type[0] ≝
   One  : Formula
 | Atom : nat → Formula
 | NAtom: nat → Formula
 | Neg  : Formula → Formula
 | Times: Formula → Formula → Formula
 | Par  : Formula → Formula → Formula.

(* Unit: notation and interpretation *)
notation "𝟙" with precedence 90 for @{ 'One }.
interpretation "One" 'One = One.

(* Atom: notation and interpretation *)
notation "hvbox(𝔸 \sub n)" with precedence 90 for @{ 'Atom $n }.
interpretation "Atom" 'Atom n = (Atom n).

(* Negative atom: notation and interpretation *)
notation "hvbox(𝔹 \sub n)" with precedence 90 for @{ 'NAtom $n }.
interpretation "NAtom" 'NAtom n = (NAtom n).

(*  Neg: notation and interpretation *)
notation "a^⊥" with precedence 90 for @{ 'Neg $a}.
interpretation "Neg" 'Neg a = (Neg a).

(* Tensor: notation and interpretation *)
notation "hvbox(a break ⊗ b)" left 
   associative with precedence 55 for @{ 'Times $a $b }.
interpretation "Times" 'Times a b = (Times a b).

(* Par: notation and interpretation *)
notation "hvbox(a break ⊠ b)" left 
   associative with precedence 50 for @{ 'Par $a $b }.
interpretation "Par" 'Par a b = (Par a b).
